Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(tt)
U12(tt) → tt
isNePal(__(I, __(P, I))) → U11(tt)

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNePal: {1}


↳ CSR
  ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(tt)
U12(tt) → tt
isNePal(__(I, __(P, I))) → U11(tt)

The replacement map contains the following entries:

__: {1, 2}
nil: empty set
U11: {1}
tt: empty set
U12: {1}
isNePal: {1}

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U12, isNePal, __1, U121, U111, ISNEPAL} are replacing on all positions.

The ordinary context-sensitive dependency pairs DPo are:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)
U111(tt) → U121(tt)
ISNEPAL(__(I, __(P, I))) → U111(tt)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(tt)
U12(tt) → tt
isNePal(__(I, __(P, I))) → U11(tt)

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 2 less nodes.


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U12, isNePal, __1} are replacing on all positions.

The TRS P consists of the following rules:

__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(tt)
U12(tt) → tt
isNePal(__(I, __(P, I))) → U11(tt)

Q is empty.

We use the subterm processor [20].


The following pairs can be oriented strictly and are deleted.


__1(__(X, Y), Z) → __1(X, __(Y, Z))
__1(__(X, Y), Z) → __1(Y, Z)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
__1(x1, x2)  =  x1

Subterm Order


↳ CSR
  ↳ CSDependencyPairsProof
    ↳ QCSDP
      ↳ QCSDependencyGraphProof
        ↳ QCSDP
          ↳ QCSDPSubtermProof
            ↳ QCSDP
              ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {__, U11, U12, isNePal} are replacing on all positions.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → U12(tt)
U12(tt) → tt
isNePal(__(I, __(P, I))) → U11(tt)

Q is empty.

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.